\begin{tabbing}
$\forall$$x$:Id, $k$:Knd, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$a$:Knd fp$\rightarrow$ Top, $f$:Top, $x_{1}$:Id, $L$:Knd List, $t$:Type.
\\[0ex]${\it ds}$ $\parallel$ $x_{1}$ : $t$
\\[0ex]$\Rightarrow$ ($x$ $=$ $x_{1}$ $\Rightarrow$ ($k$ $\in$ $L$))
\\[0ex]$\Rightarrow$ (\=with declarations \+
\\[0ex]ds:${\it ds}$
\\[0ex]da:${\it da}$
\\[0ex]effect of $k$(v) is $x$ := $f$ s v
\\[0ex]$\Vert\!+$ only members of $L$ affect $x_{1}$ :$t$)
\-
\end{tabbing}